($\lambda$$A$,$r$,$z$. WellFnd\{i\}($A$;$x$,$y$.$r$($x$,$y$))) $\in$ $A$:Type\{i\}$\rightarrow$($A$$\rightarrow$$A$$\rightarrow\mathbb{P}$\{i\})$\rightarrow$($\downarrow$True)$\rightarrow\mathbb{P}$\{i'\}